(declare-fun f () String)
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun g () String)
(declare-fun c () String)
(declare-fun d () String)
(declare-fun shifted_T4_3 () String)
(declare-fun shifted_T5_3 () String)
(declare-fun e () Bool)
(assert (ite e (and (= b a (str.len shifted_T4_3) 0 (str.len (str.substr f 0 (str.len g)))) (= c d shifted_T5_3 "?")) (and (= b 0) (not (str.in.re c (str.to.re "?"))))))
(check-sat)
